The invention relates to a method of verifying a mathematical proof which is formulated in a typed higher-order language. The fact that a language is a typed higher-order language means that it contains typed terms and that so-called higher-order constructs are used. The language is chosen because it is better suited to the normal mathematical formulations than the so-called first order languages. The latter languages are more frequently used because of their simple structure, but have less power of expression due to limitations to the constructs to be used. An example of such a typed higher-order language and its use is described in L. S. van Benthem Jutting, Checking Landau's "Grundlagen" in the Automath System, Mathematical Centre Tracts, Vol. 83, Amsterdam, 1979. A typed higher-order language is a logic language which is composed of terms, categories of terms being: types, expressions, "ordinary" terms, proofs, propositions, abbreviations, being names for respective other terms; in this respect a variety of categories of terms is permissible. The expression of a term may be, for example a constant, a variable or a function. The terms are linked by constructors indicating relationships between terms. Constructors can indicate arithmetical operations, logic operations, implications and so on. Such a language can be used in order to formulate a mathematical proof, where each of the various parts of the proof is given a name and is included in a hierarchical structure of parts of each time higher order until a name of highest order is given. Such a proof is then formulated in a sequence of lines, each line in the sequence being not lower in the hierarchy than all preceding lines in the sequence. This means: the later line is either higher in the hierarchy or no relationship exists between the two lines.
For the method of verifying a mathematical proof consisting of a number of sub-proofs it is necessary that the following requirements are satisfied for the successive assignment of the abbreviations or lines:
1. A series of verifications must be performed on the "lines"; PA0 2. Each "line" is influenced by an environment in which zero or more other "lines" are present which occupy a preceding position in the sequence and hence have a lower level in the hierarchy; PA0 3. The result of the verification of a "line" is determined by all lines in the environment; it is not necessary for all such environmental lines to make also a material contribution to the determination thereof; PA0 4. When all "lines" in the relevant environment are correct, the verification of the relevant line can be executed in a finite number of steps and offer the result "correct" or "error". The period of time required is also finite and depends on the processing speed. PA0 5. However, when one or more "lines" in the relevant environment are not correct, a third result is feasible in that the number of steps required becomes infinitely large, notably because the verification process starts to circulate infinitely long in a loop. The verification of the proof in the sequence of the lines, therefore, always offers a correct answer within a finite period, but because of the large number of steps required this period of time is sometimes unacceptably long. PA0 during a distribution process successive sub-sequences of lines are formed from the first sequence of lines; PA0 the distribution process each time assigns a next sub-sequence to an available verification process of a second series of verification processes for the purpose of verification, a verification process receiving not only a sub-sequence assigned thereto but also all preceding sub-sequences in order to abstract from said preceding sub-sequences the type definition of the names occurring in the assigned sub-sequence; PA0 the series of verification processes execute the verifications, a positive verification resulting in a "ready" signal, a negative verification resulting in an "error" signal, and a non-interrupted verification providing neither a "ready" signal nor an "error" signal; PA0 upon reception of an "error" signal, the distribution process delivers a stop signal to all verification processes, but upon reception of an adequate number of "ready" signals, it provides an "OK" signal to a user. The successive assignment of the sub-sequences in sequence to the verification processes must be performed so that, if no verification process is available, i.e. they are all busy, a sequence of consecutive sub-sequences is being processed: thus, no sub-sequence has been skipped. When this condition is satisfied, it is not strictly necessary to adhere to the assignment sequence at the level of the sub-sequence; however, at the level of the series of verification processes it must be maintained.